Fixed Points meet Löb's Rule

Abstract: The modal part of the work reported in this talk is in collaboration with Tadeusz Litak.

For a wide class of theories we have the Second Incompleteness Theorem and, what is more, Löb's rule, also in cases where the third Löb Condition L3 *provable implies provably provable* (aka 4) fails. We will briefly indicate some examples of this phenomenon. What happens when we do have Löb's Rule but not L3? It turns out that we still have a lot. For example, the de Jongh-Sambin-Bernardi Theorem on the uniqueness of fixed points remains valid. So, e.g., Gödel sentences are unique modulo provable equivalence. On the other hand, explicit definability of fixed points fails. An arithmetical example of the non-explicit-definability of the Gödel sentence is still lacking. (I do have an arithmetical example where the Gödel sentence is equivalent to the consistency of inconsistency but not to consistency.)

We discuss the relevant logic: the Henkin Calculus, to wit, K plus Löb's rule plus boxed fixed points. This logic turns out to be synonymous to the mu-calculus plus the minimal Henkin sentence, which expresses well-foundedness. So, results concerning the mu-calculus, like uniform interpolation, can be transferred to the Henkin Calculus.

logic in computer sciencelogic

Audience: researchers in the topic

Proof Theory Virtual Seminar

Series comments: The Proof Theory Virtual Seminar presents talks by leading researchers from all areas of proof theory. Everyone who is interested in the subject is warmly invited to attend! In order to participate, please visit the seminar webpage: www.proofsociety.org/proof-theory-seminar/